The calculus of inductive constructions is the underlying core language of the Coq Proof Assistant. It is based on the calculus of constructions extended by inductive definitions as they are known from intuitionistic type theory.
http://coq.inria.fr/doc/Reference-Manual006.html